Nuprl Definition : ma-single-pre-init1
0,22
postcript
pdf
ma-single-pre-init1(
x
;
T
;
c
;
a
;
T'
;
y
,
v
.
P
(
y
;
v
))
== with ds:
x
:
T
init:
x
:
c
action
a
:
T'
precondition
a
(v) is
s
,
v
.
P
(
s
(
x
);
v
)
latex
Definitions
x
:
v
,
with ds:
ds
init:
init
action
a
:
T
precondition
a
(v) is
P
,
ma-single-pre-init1(
x
;
T
;
c
;
a
;
T'
;
y
,
v
.
P
(
y
;
v
))
FDL editor aliases
ma-single-pre-init1
origin
s,v. P(s(x);v) s,v. P(s(x);v)